﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using System.Diagnostics.Contracts;
using FazaDemo.BL.InterfaceDomain;
using FazaDemo.BL.Services_;
using FazaDemo.BL.SubDomains;

namespace FazaDemo.BL.Services_
{
    [ContractClassFor(typeof(INavCondConverter))]
    abstract class NavCondConverterContract : INavCondConverter
    {
        public NavigatorCondition GenerateCondition(string ecqText)
        {
            Contract.Ensures(Contract.Result<NavigatorCondition>().Tittle != null);
            Contract.Ensures(Contract.Result<NavigatorCondition>().Tittle.Any());
            Contract.Ensures(Contract.Result<NavigatorCondition>().CondElements != null);
            Contract.Ensures(Contract.Result<NavigatorCondition>().CondElements.Any());
            Contract.Ensures(Contract.Result<NavigatorCondition>().CondElements.Any(e => e.ElemText != null));
            Contract.Ensures(Contract.Result<NavigatorCondition>().CondElements.Any(e => e.ElemText.Any()));
            return default(NavigatorCondition);
        }
    }
}
